Problem:
 __(__(X,Y),Z) -> __(X,__(Y,Z))
 __(X,nil()) -> X
 __(nil(),X) -> X
 and(tt(),X) -> activate(X)
 isList(V) -> isNeList(activate(V))
 isList(n__nil()) -> tt()
 isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
 isNeList(V) -> isQid(activate(V))
 isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
 isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
 isNePal(V) -> isQid(activate(V))
 isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
 isPal(V) -> isNePal(activate(V))
 isPal(n__nil()) -> tt()
 isQid(n__a()) -> tt()
 isQid(n__e()) -> tt()
 isQid(n__i()) -> tt()
 isQid(n__o()) -> tt()
 isQid(n__u()) -> tt()
 nil() -> n__nil()
 __(X1,X2) -> n____(X1,X2)
 isList(X) -> n__isList(X)
 isNeList(X) -> n__isNeList(X)
 isPal(X) -> n__isPal(X)
 a() -> n__a()
 e() -> n__e()
 i() -> n__i()
 o() -> n__o()
 u() -> n__u()
 activate(n__nil()) -> nil()
 activate(n____(X1,X2)) -> __(X1,X2)
 activate(n__isList(X)) -> isList(X)
 activate(n__isNeList(X)) -> isNeList(X)
 activate(n__isPal(X)) -> isPal(X)
 activate(n__a()) -> a()
 activate(n__e()) -> e()
 activate(n__i()) -> i()
 activate(n__o()) -> o()
 activate(n__u()) -> u()
 activate(X) -> X

Proof:
 Complexity Transformation Processor:
  strict:
   __(__(X,Y),Z) -> __(X,__(Y,Z))
   __(X,nil()) -> X
   __(nil(),X) -> X
   and(tt(),X) -> activate(X)
   isList(V) -> isNeList(activate(V))
   isList(n__nil()) -> tt()
   isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
   isNeList(V) -> isQid(activate(V))
   isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
   isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
   isNePal(V) -> isQid(activate(V))
   isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
   isPal(V) -> isNePal(activate(V))
   isPal(n__nil()) -> tt()
   isQid(n__a()) -> tt()
   isQid(n__e()) -> tt()
   isQid(n__i()) -> tt()
   isQid(n__o()) -> tt()
   isQid(n__u()) -> tt()
   nil() -> n__nil()
   __(X1,X2) -> n____(X1,X2)
   isList(X) -> n__isList(X)
   isNeList(X) -> n__isNeList(X)
   isPal(X) -> n__isPal(X)
   a() -> n__a()
   e() -> n__e()
   i() -> n__i()
   o() -> n__o()
   u() -> n__u()
   activate(n__nil()) -> nil()
   activate(n____(X1,X2)) -> __(X1,X2)
   activate(n__isList(X)) -> isList(X)
   activate(n__isNeList(X)) -> isNeList(X)
   activate(n__isPal(X)) -> isPal(X)
   activate(n__a()) -> a()
   activate(n__e()) -> e()
   activate(n__i()) -> i()
   activate(n__o()) -> o()
   activate(n__u()) -> u()
   activate(X) -> X
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [u] = 0,
     
     [o] = 0,
     
     [i] = 0,
     
     [e] = 0,
     
     [a] = 0,
     
     [n__u] = 8,
     
     [n__o] = 12,
     
     [n__i] = 1,
     
     [n__e] = 0,
     
     [n__a] = 0,
     
     [isPal](x0) = x0,
     
     [n__isPal](x0) = x0,
     
     [isNePal](x0) = x0,
     
     [n__isNeList](x0) = x0 + 12,
     
     [isQid](x0) = x0 + 4,
     
     [n__isList](x0) = x0,
     
     [n____](x0, x1) = x0 + x1 + 13,
     
     [n__nil] = 5,
     
     [isNeList](x0) = x0 + 1,
     
     [isList](x0) = x0,
     
     [activate](x0) = x0 + 8,
     
     [and](x0, x1) = x0 + x1 + 3,
     
     [tt] = 0,
     
     [nil] = 4,
     
     [__](x0, x1) = x0 + x1 + 13
    orientation:
     __(__(X,Y),Z) = X + Y + Z + 26 >= X + Y + Z + 26 = __(X,__(Y,Z))
     
     __(X,nil()) = X + 17 >= X = X
     
     __(nil(),X) = X + 17 >= X = X
     
     and(tt(),X) = X + 3 >= X + 8 = activate(X)
     
     isList(V) = V >= V + 9 = isNeList(activate(V))
     
     isList(n__nil()) = 5 >= 0 = tt()
     
     isList(n____(V1,V2)) = V1 + V2 + 13 >= V1 + V2 + 19 = and(isList(activate(V1)),n__isList(activate(V2)))
     
     isNeList(V) = V + 1 >= V + 12 = isQid(activate(V))
     
     isNeList(n____(V1,V2)) = V1 + V2 + 14 >= V1 + V2 + 31 = and(isList(activate(V1)),n__isNeList(activate(V2)))
     
     isNeList(n____(V1,V2)) = V1 + V2 + 14 >= V1 + V2 + 20 = and(isNeList(activate(V1)),n__isList(activate(V2)))
     
     isNePal(V) = V >= V + 12 = isQid(activate(V))
     
     isNePal(n____(I,__(P,I))) = 2I + P + 26 >= I + P + 23 = and(isQid(activate(I)),n__isPal(activate(P)))
     
     isPal(V) = V >= V + 8 = isNePal(activate(V))
     
     isPal(n__nil()) = 5 >= 0 = tt()
     
     isQid(n__a()) = 4 >= 0 = tt()
     
     isQid(n__e()) = 4 >= 0 = tt()
     
     isQid(n__i()) = 5 >= 0 = tt()
     
     isQid(n__o()) = 16 >= 0 = tt()
     
     isQid(n__u()) = 12 >= 0 = tt()
     
     nil() = 4 >= 5 = n__nil()
     
     __(X1,X2) = X1 + X2 + 13 >= X1 + X2 + 13 = n____(X1,X2)
     
     isList(X) = X >= X = n__isList(X)
     
     isNeList(X) = X + 1 >= X + 12 = n__isNeList(X)
     
     isPal(X) = X >= X = n__isPal(X)
     
     a() = 0 >= 0 = n__a()
     
     e() = 0 >= 0 = n__e()
     
     i() = 0 >= 1 = n__i()
     
     o() = 0 >= 12 = n__o()
     
     u() = 0 >= 8 = n__u()
     
     activate(n__nil()) = 13 >= 4 = nil()
     
     activate(n____(X1,X2)) = X1 + X2 + 21 >= X1 + X2 + 13 = __(X1,X2)
     
     activate(n__isList(X)) = X + 8 >= X = isList(X)
     
     activate(n__isNeList(X)) = X + 20 >= X + 1 = isNeList(X)
     
     activate(n__isPal(X)) = X + 8 >= X = isPal(X)
     
     activate(n__a()) = 8 >= 0 = a()
     
     activate(n__e()) = 8 >= 0 = e()
     
     activate(n__i()) = 9 >= 0 = i()
     
     activate(n__o()) = 20 >= 0 = o()
     
     activate(n__u()) = 16 >= 0 = u()
     
     activate(X) = X + 8 >= X = X
    problem:
     strict:
      __(__(X,Y),Z) -> __(X,__(Y,Z))
      and(tt(),X) -> activate(X)
      isList(V) -> isNeList(activate(V))
      isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
      isNeList(V) -> isQid(activate(V))
      isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
      isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
      isNePal(V) -> isQid(activate(V))
      isPal(V) -> isNePal(activate(V))
      nil() -> n__nil()
      __(X1,X2) -> n____(X1,X2)
      isList(X) -> n__isList(X)
      isNeList(X) -> n__isNeList(X)
      isPal(X) -> n__isPal(X)
      a() -> n__a()
      e() -> n__e()
      i() -> n__i()
      o() -> n__o()
      u() -> n__u()
     weak:
      __(X,nil()) -> X
      __(nil(),X) -> X
      isList(n__nil()) -> tt()
      isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
      isPal(n__nil()) -> tt()
      isQid(n__a()) -> tt()
      isQid(n__e()) -> tt()
      isQid(n__i()) -> tt()
      isQid(n__o()) -> tt()
      isQid(n__u()) -> tt()
      activate(n__nil()) -> nil()
      activate(n____(X1,X2)) -> __(X1,X2)
      activate(n__isList(X)) -> isList(X)
      activate(n__isNeList(X)) -> isNeList(X)
      activate(n__isPal(X)) -> isPal(X)
      activate(n__a()) -> a()
      activate(n__e()) -> e()
      activate(n__i()) -> i()
      activate(n__o()) -> o()
      activate(n__u()) -> u()
      activate(X) -> X
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [u] = 3,
       
       [o] = 0,
       
       [i] = 2,
       
       [e] = 0,
       
       [a] = 0,
       
       [n__u] = 2,
       
       [n__o] = 10,
       
       [n__i] = 0,
       
       [n__e] = 0,
       
       [n__a] = 0,
       
       [isPal](x0) = x0 + 8,
       
       [n__isPal](x0) = x0 + 8,
       
       [isNePal](x0) = x0 + 12,
       
       [n__isNeList](x0) = x0,
       
       [isQid](x0) = x0 + 1,
       
       [n__isList](x0) = x0 + 2,
       
       [n____](x0, x1) = x0 + x1 + 10,
       
       [n__nil] = 0,
       
       [isNeList](x0) = x0 + 2,
       
       [isList](x0) = x0,
       
       [activate](x0) = x0 + 2,
       
       [and](x0, x1) = x0 + x1 + 9,
       
       [tt] = 0,
       
       [nil] = 0,
       
       [__](x0, x1) = x0 + x1
      orientation:
       __(__(X,Y),Z) = X + Y + Z >= X + Y + Z = __(X,__(Y,Z))
       
       and(tt(),X) = X + 9 >= X + 2 = activate(X)
       
       isList(V) = V >= V + 4 = isNeList(activate(V))
       
       isList(n____(V1,V2)) = V1 + V2 + 10 >= V1 + V2 + 15 = and(isList(activate(V1)),n__isList(activate(V2)))
       
       isNeList(V) = V + 2 >= V + 3 = isQid(activate(V))
       
       isNeList(n____(V1,V2)) = V1 + V2 + 12 >= V1 + V2 + 13 = and(isList(activate(V1)),n__isNeList(activate(V2)))
       
       isNeList(n____(V1,V2)) = V1 + V2 + 12 >= V1 + V2 + 17 = and(isNeList(activate(V1)),n__isList(activate(V2)))
       
       isNePal(V) = V + 12 >= V + 3 = isQid(activate(V))
       
       isPal(V) = V + 8 >= V + 14 = isNePal(activate(V))
       
       nil() = 0 >= 0 = n__nil()
       
       __(X1,X2) = X1 + X2 >= X1 + X2 + 10 = n____(X1,X2)
       
       isList(X) = X >= X + 2 = n__isList(X)
       
       isNeList(X) = X + 2 >= X = n__isNeList(X)
       
       isPal(X) = X + 8 >= X + 8 = n__isPal(X)
       
       a() = 0 >= 0 = n__a()
       
       e() = 0 >= 0 = n__e()
       
       i() = 2 >= 0 = n__i()
       
       o() = 0 >= 10 = n__o()
       
       u() = 3 >= 2 = n__u()
       
       __(X,nil()) = X >= X = X
       
       __(nil(),X) = X >= X = X
       
       isList(n__nil()) = 0 >= 0 = tt()
       
       isNePal(n____(I,__(P,I))) = 2I + P + 22 >= I + P + 22 = and(isQid(activate(I)),n__isPal(activate(P)))
       
       isPal(n__nil()) = 8 >= 0 = tt()
       
       isQid(n__a()) = 1 >= 0 = tt()
       
       isQid(n__e()) = 1 >= 0 = tt()
       
       isQid(n__i()) = 1 >= 0 = tt()
       
       isQid(n__o()) = 11 >= 0 = tt()
       
       isQid(n__u()) = 3 >= 0 = tt()
       
       activate(n__nil()) = 2 >= 0 = nil()
       
       activate(n____(X1,X2)) = X1 + X2 + 12 >= X1 + X2 = __(X1,X2)
       
       activate(n__isList(X)) = X + 4 >= X = isList(X)
       
       activate(n__isNeList(X)) = X + 2 >= X + 2 = isNeList(X)
       
       activate(n__isPal(X)) = X + 10 >= X + 8 = isPal(X)
       
       activate(n__a()) = 2 >= 0 = a()
       
       activate(n__e()) = 2 >= 0 = e()
       
       activate(n__i()) = 2 >= 2 = i()
       
       activate(n__o()) = 12 >= 0 = o()
       
       activate(n__u()) = 4 >= 3 = u()
       
       activate(X) = X + 2 >= X = X
      problem:
       strict:
        __(__(X,Y),Z) -> __(X,__(Y,Z))
        isList(V) -> isNeList(activate(V))
        isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
        isNeList(V) -> isQid(activate(V))
        isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
        isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
        isPal(V) -> isNePal(activate(V))
        nil() -> n__nil()
        __(X1,X2) -> n____(X1,X2)
        isList(X) -> n__isList(X)
        isPal(X) -> n__isPal(X)
        a() -> n__a()
        e() -> n__e()
        o() -> n__o()
       weak:
        and(tt(),X) -> activate(X)
        isNePal(V) -> isQid(activate(V))
        isNeList(X) -> n__isNeList(X)
        i() -> n__i()
        u() -> n__u()
        __(X,nil()) -> X
        __(nil(),X) -> X
        isList(n__nil()) -> tt()
        isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
        isPal(n__nil()) -> tt()
        isQid(n__a()) -> tt()
        isQid(n__e()) -> tt()
        isQid(n__i()) -> tt()
        isQid(n__o()) -> tt()
        isQid(n__u()) -> tt()
        activate(n__nil()) -> nil()
        activate(n____(X1,X2)) -> __(X1,X2)
        activate(n__isList(X)) -> isList(X)
        activate(n__isNeList(X)) -> isNeList(X)
        activate(n__isPal(X)) -> isPal(X)
        activate(n__a()) -> a()
        activate(n__e()) -> e()
        activate(n__i()) -> i()
        activate(n__o()) -> o()
        activate(n__u()) -> u()
        activate(X) -> X
      Matrix Interpretation Processor:
       dimension: 1
       max_matrix:
        1
        interpretation:
         [u] = 7,
         
         [o] = 0,
         
         [i] = 0,
         
         [e] = 0,
         
         [a] = 1,
         
         [n__u] = 7,
         
         [n__o] = 1,
         
         [n__i] = 0,
         
         [n__e] = 10,
         
         [n__a] = 0,
         
         [isPal](x0) = x0 + 5,
         
         [n__isPal](x0) = x0 + 4,
         
         [isNePal](x0) = x0 + 2,
         
         [n__isNeList](x0) = x0 + 15,
         
         [isQid](x0) = x0 + 1,
         
         [n__isList](x0) = x0 + 6,
         
         [n____](x0, x1) = x0 + x1 + 7,
         
         [n__nil] = 1,
         
         [isNeList](x0) = x0 + 15,
         
         [isList](x0) = x0,
         
         [activate](x0) = x0 + 1,
         
         [and](x0, x1) = x0 + x1,
         
         [tt] = 1,
         
         [nil] = 0,
         
         [__](x0, x1) = x0 + x1
        orientation:
         __(__(X,Y),Z) = X + Y + Z >= X + Y + Z = __(X,__(Y,Z))
         
         isList(V) = V >= V + 16 = isNeList(activate(V))
         
         isList(n____(V1,V2)) = V1 + V2 + 7 >= V1 + V2 + 8 = and(isList(activate(V1)),n__isList(activate(V2)))
         
         isNeList(V) = V + 15 >= V + 2 = isQid(activate(V))
         
         isNeList(n____(V1,V2)) = V1 + V2 + 22 >= V1 + V2 + 17 = and(isList(activate(V1)),n__isNeList(activate(V2)))
         
         isNeList(n____(V1,V2)) = V1 + V2 + 22 >= V1 + V2 + 23 = and(isNeList(activate(V1)),n__isList(activate(V2)))
         
         isPal(V) = V + 5 >= V + 3 = isNePal(activate(V))
         
         nil() = 0 >= 1 = n__nil()
         
         __(X1,X2) = X1 + X2 >= X1 + X2 + 7 = n____(X1,X2)
         
         isList(X) = X >= X + 6 = n__isList(X)
         
         isPal(X) = X + 5 >= X + 4 = n__isPal(X)
         
         a() = 1 >= 0 = n__a()
         
         e() = 0 >= 10 = n__e()
         
         o() = 0 >= 1 = n__o()
         
         and(tt(),X) = X + 1 >= X + 1 = activate(X)
         
         isNePal(V) = V + 2 >= V + 2 = isQid(activate(V))
         
         isNeList(X) = X + 15 >= X + 15 = n__isNeList(X)
         
         i() = 0 >= 0 = n__i()
         
         u() = 7 >= 7 = n__u()
         
         __(X,nil()) = X >= X = X
         
         __(nil(),X) = X >= X = X
         
         isList(n__nil()) = 1 >= 1 = tt()
         
         isNePal(n____(I,__(P,I))) = 2I + P + 9 >= I + P + 7 = and(isQid(activate(I)),n__isPal(activate(P)))
         
         isPal(n__nil()) = 6 >= 1 = tt()
         
         isQid(n__a()) = 1 >= 1 = tt()
         
         isQid(n__e()) = 11 >= 1 = tt()
         
         isQid(n__i()) = 1 >= 1 = tt()
         
         isQid(n__o()) = 2 >= 1 = tt()
         
         isQid(n__u()) = 8 >= 1 = tt()
         
         activate(n__nil()) = 2 >= 0 = nil()
         
         activate(n____(X1,X2)) = X1 + X2 + 8 >= X1 + X2 = __(X1,X2)
         
         activate(n__isList(X)) = X + 7 >= X = isList(X)
         
         activate(n__isNeList(X)) = X + 16 >= X + 15 = isNeList(X)
         
         activate(n__isPal(X)) = X + 5 >= X + 5 = isPal(X)
         
         activate(n__a()) = 1 >= 1 = a()
         
         activate(n__e()) = 11 >= 0 = e()
         
         activate(n__i()) = 1 >= 0 = i()
         
         activate(n__o()) = 2 >= 0 = o()
         
         activate(n__u()) = 8 >= 7 = u()
         
         activate(X) = X + 1 >= X = X
        problem:
         strict:
          __(__(X,Y),Z) -> __(X,__(Y,Z))
          isList(V) -> isNeList(activate(V))
          isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
          isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
          nil() -> n__nil()
          __(X1,X2) -> n____(X1,X2)
          isList(X) -> n__isList(X)
          e() -> n__e()
          o() -> n__o()
         weak:
          isNeList(V) -> isQid(activate(V))
          isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
          isPal(V) -> isNePal(activate(V))
          isPal(X) -> n__isPal(X)
          a() -> n__a()
          and(tt(),X) -> activate(X)
          isNePal(V) -> isQid(activate(V))
          isNeList(X) -> n__isNeList(X)
          i() -> n__i()
          u() -> n__u()
          __(X,nil()) -> X
          __(nil(),X) -> X
          isList(n__nil()) -> tt()
          isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
          isPal(n__nil()) -> tt()
          isQid(n__a()) -> tt()
          isQid(n__e()) -> tt()
          isQid(n__i()) -> tt()
          isQid(n__o()) -> tt()
          isQid(n__u()) -> tt()
          activate(n__nil()) -> nil()
          activate(n____(X1,X2)) -> __(X1,X2)
          activate(n__isList(X)) -> isList(X)
          activate(n__isNeList(X)) -> isNeList(X)
          activate(n__isPal(X)) -> isPal(X)
          activate(n__a()) -> a()
          activate(n__e()) -> e()
          activate(n__i()) -> i()
          activate(n__o()) -> o()
          activate(n__u()) -> u()
          activate(X) -> X
        Matrix Interpretation Processor:
         dimension: 1
         max_matrix:
          1
          interpretation:
           [u] = 4,
           
           [o] = 3,
           
           [i] = 14,
           
           [e] = 0,
           
           [a] = 5,
           
           [n__u] = 4,
           
           [n__o] = 2,
           
           [n__i] = 12,
           
           [n__e] = 6,
           
           [n__a] = 5,
           
           [isPal](x0) = x0 + 4,
           
           [n__isPal](x0) = x0 + 4,
           
           [isNePal](x0) = x0 + 2,
           
           [n__isNeList](x0) = x0 + 2,
           
           [isQid](x0) = x0,
           
           [n__isList](x0) = x0 + 8,
           
           [n____](x0, x1) = x0 + x1 + 10,
           
           [n__nil] = 11,
           
           [isNeList](x0) = x0 + 2,
           
           [isList](x0) = x0 + 6,
           
           [activate](x0) = x0 + 2,
           
           [and](x0, x1) = x0 + x1,
           
           [tt] = 2,
           
           [nil] = 8,
           
           [__](x0, x1) = x0 + x1 + 1
          orientation:
           __(__(X,Y),Z) = X + Y + Z + 2 >= X + Y + Z + 2 = __(X,__(Y,Z))
           
           isList(V) = V + 6 >= V + 4 = isNeList(activate(V))
           
           isList(n____(V1,V2)) = V1 + V2 + 16 >= V1 + V2 + 18 = and(isList(activate(V1)),n__isList(activate(V2)))
           
           isNeList(n____(V1,V2)) = V1 + V2 + 12 >= V1 + V2 + 14 = and(isNeList(activate(V1)),n__isList(activate(V2)))
           
           nil() = 8 >= 11 = n__nil()
           
           __(X1,X2) = X1 + X2 + 1 >= X1 + X2 + 10 = n____(X1,X2)
           
           isList(X) = X + 6 >= X + 8 = n__isList(X)
           
           e() = 0 >= 6 = n__e()
           
           o() = 3 >= 2 = n__o()
           
           isNeList(V) = V + 2 >= V + 2 = isQid(activate(V))
           
           isNeList(n____(V1,V2)) = V1 + V2 + 12 >= V1 + V2 + 12 = and(isList(activate(V1)),n__isNeList(activate(V2)))
           
           isPal(V) = V + 4 >= V + 4 = isNePal(activate(V))
           
           isPal(X) = X + 4 >= X + 4 = n__isPal(X)
           
           a() = 5 >= 5 = n__a()
           
           and(tt(),X) = X + 2 >= X + 2 = activate(X)
           
           isNePal(V) = V + 2 >= V + 2 = isQid(activate(V))
           
           isNeList(X) = X + 2 >= X + 2 = n__isNeList(X)
           
           i() = 14 >= 12 = n__i()
           
           u() = 4 >= 4 = n__u()
           
           __(X,nil()) = X + 9 >= X = X
           
           __(nil(),X) = X + 9 >= X = X
           
           isList(n__nil()) = 17 >= 2 = tt()
           
           isNePal(n____(I,__(P,I))) = 2I + P + 13 >= I + P + 8 = and(isQid(activate(I)),n__isPal(activate(P)))
           
           isPal(n__nil()) = 15 >= 2 = tt()
           
           isQid(n__a()) = 5 >= 2 = tt()
           
           isQid(n__e()) = 6 >= 2 = tt()
           
           isQid(n__i()) = 12 >= 2 = tt()
           
           isQid(n__o()) = 2 >= 2 = tt()
           
           isQid(n__u()) = 4 >= 2 = tt()
           
           activate(n__nil()) = 13 >= 8 = nil()
           
           activate(n____(X1,X2)) = X1 + X2 + 12 >= X1 + X2 + 1 = __(X1,X2)
           
           activate(n__isList(X)) = X + 10 >= X + 6 = isList(X)
           
           activate(n__isNeList(X)) = X + 4 >= X + 2 = isNeList(X)
           
           activate(n__isPal(X)) = X + 6 >= X + 4 = isPal(X)
           
           activate(n__a()) = 7 >= 5 = a()
           
           activate(n__e()) = 8 >= 0 = e()
           
           activate(n__i()) = 14 >= 14 = i()
           
           activate(n__o()) = 4 >= 3 = o()
           
           activate(n__u()) = 6 >= 4 = u()
           
           activate(X) = X + 2 >= X = X
          problem:
           strict:
            __(__(X,Y),Z) -> __(X,__(Y,Z))
            isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
            isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
            nil() -> n__nil()
            __(X1,X2) -> n____(X1,X2)
            isList(X) -> n__isList(X)
            e() -> n__e()
           weak:
            isList(V) -> isNeList(activate(V))
            o() -> n__o()
            isNeList(V) -> isQid(activate(V))
            isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
            isPal(V) -> isNePal(activate(V))
            isPal(X) -> n__isPal(X)
            a() -> n__a()
            and(tt(),X) -> activate(X)
            isNePal(V) -> isQid(activate(V))
            isNeList(X) -> n__isNeList(X)
            i() -> n__i()
            u() -> n__u()
            __(X,nil()) -> X
            __(nil(),X) -> X
            isList(n__nil()) -> tt()
            isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
            isPal(n__nil()) -> tt()
            isQid(n__a()) -> tt()
            isQid(n__e()) -> tt()
            isQid(n__i()) -> tt()
            isQid(n__o()) -> tt()
            isQid(n__u()) -> tt()
            activate(n__nil()) -> nil()
            activate(n____(X1,X2)) -> __(X1,X2)
            activate(n__isList(X)) -> isList(X)
            activate(n__isNeList(X)) -> isNeList(X)
            activate(n__isPal(X)) -> isPal(X)
            activate(n__a()) -> a()
            activate(n__e()) -> e()
            activate(n__i()) -> i()
            activate(n__o()) -> o()
            activate(n__u()) -> u()
            activate(X) -> X
          Matrix Interpretation Processor:
           dimension: 1
           max_matrix:
            1
            interpretation:
             [u] = 9,
             
             [o] = 8,
             
             [i] = 12,
             
             [e] = 13,
             
             [a] = 8,
             
             [n__u] = 9,
             
             [n__o] = 8,
             
             [n__i] = 12,
             
             [n__e] = 12,
             
             [n__a] = 8,
             
             [isPal](x0) = x0 + 15,
             
             [n__isPal](x0) = x0 + 15,
             
             [isNePal](x0) = x0 + 14,
             
             [n__isNeList](x0) = x0 + 2,
             
             [isQid](x0) = x0 + 1,
             
             [n__isList](x0) = x0 + 2,
             
             [n____](x0, x1) = x0 + x1 + 5,
             
             [n__nil] = 8,
             
             [isNeList](x0) = x0 + 2,
             
             [isList](x0) = x0 + 3,
             
             [activate](x0) = x0 + 1,
             
             [and](x0, x1) = x0 + x1,
             
             [tt] = 1,
             
             [nil] = 0,
             
             [__](x0, x1) = x0 + x1
            orientation:
             __(__(X,Y),Z) = X + Y + Z >= X + Y + Z = __(X,__(Y,Z))
             
             isList(n____(V1,V2)) = V1 + V2 + 8 >= V1 + V2 + 7 = and(isList(activate(V1)),n__isList(activate(V2)))
             
             isNeList(n____(V1,V2)) = V1 + V2 + 7 >= V1 + V2 + 6 = and(isNeList(activate(V1)),n__isList(activate(V2)))
             
             nil() = 0 >= 8 = n__nil()
             
             __(X1,X2) = X1 + X2 >= X1 + X2 + 5 = n____(X1,X2)
             
             isList(X) = X + 3 >= X + 2 = n__isList(X)
             
             e() = 13 >= 12 = n__e()
             
             isList(V) = V + 3 >= V + 3 = isNeList(activate(V))
             
             o() = 8 >= 8 = n__o()
             
             isNeList(V) = V + 2 >= V + 2 = isQid(activate(V))
             
             isNeList(n____(V1,V2)) = V1 + V2 + 7 >= V1 + V2 + 7 = and(isList(activate(V1)),n__isNeList(activate(V2)))
             
             isPal(V) = V + 15 >= V + 15 = isNePal(activate(V))
             
             isPal(X) = X + 15 >= X + 15 = n__isPal(X)
             
             a() = 8 >= 8 = n__a()
             
             and(tt(),X) = X + 1 >= X + 1 = activate(X)
             
             isNePal(V) = V + 14 >= V + 2 = isQid(activate(V))
             
             isNeList(X) = X + 2 >= X + 2 = n__isNeList(X)
             
             i() = 12 >= 12 = n__i()
             
             u() = 9 >= 9 = n__u()
             
             __(X,nil()) = X >= X = X
             
             __(nil(),X) = X >= X = X
             
             isList(n__nil()) = 11 >= 1 = tt()
             
             isNePal(n____(I,__(P,I))) = 2I + P + 19 >= I + P + 18 = and(isQid(activate(I)),n__isPal(activate(P)))
             
             isPal(n__nil()) = 23 >= 1 = tt()
             
             isQid(n__a()) = 9 >= 1 = tt()
             
             isQid(n__e()) = 13 >= 1 = tt()
             
             isQid(n__i()) = 13 >= 1 = tt()
             
             isQid(n__o()) = 9 >= 1 = tt()
             
             isQid(n__u()) = 10 >= 1 = tt()
             
             activate(n__nil()) = 9 >= 0 = nil()
             
             activate(n____(X1,X2)) = X1 + X2 + 6 >= X1 + X2 = __(X1,X2)
             
             activate(n__isList(X)) = X + 3 >= X + 3 = isList(X)
             
             activate(n__isNeList(X)) = X + 3 >= X + 2 = isNeList(X)
             
             activate(n__isPal(X)) = X + 16 >= X + 15 = isPal(X)
             
             activate(n__a()) = 9 >= 8 = a()
             
             activate(n__e()) = 13 >= 13 = e()
             
             activate(n__i()) = 13 >= 12 = i()
             
             activate(n__o()) = 9 >= 8 = o()
             
             activate(n__u()) = 10 >= 9 = u()
             
             activate(X) = X + 1 >= X = X
            problem:
             strict:
              __(__(X,Y),Z) -> __(X,__(Y,Z))
              nil() -> n__nil()
              __(X1,X2) -> n____(X1,X2)
             weak:
              isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
              isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
              isList(X) -> n__isList(X)
              e() -> n__e()
              isList(V) -> isNeList(activate(V))
              o() -> n__o()
              isNeList(V) -> isQid(activate(V))
              isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
              isPal(V) -> isNePal(activate(V))
              isPal(X) -> n__isPal(X)
              a() -> n__a()
              and(tt(),X) -> activate(X)
              isNePal(V) -> isQid(activate(V))
              isNeList(X) -> n__isNeList(X)
              i() -> n__i()
              u() -> n__u()
              __(X,nil()) -> X
              __(nil(),X) -> X
              isList(n__nil()) -> tt()
              isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
              isPal(n__nil()) -> tt()
              isQid(n__a()) -> tt()
              isQid(n__e()) -> tt()
              isQid(n__i()) -> tt()
              isQid(n__o()) -> tt()
              isQid(n__u()) -> tt()
              activate(n__nil()) -> nil()
              activate(n____(X1,X2)) -> __(X1,X2)
              activate(n__isList(X)) -> isList(X)
              activate(n__isNeList(X)) -> isNeList(X)
              activate(n__isPal(X)) -> isPal(X)
              activate(n__a()) -> a()
              activate(n__e()) -> e()
              activate(n__i()) -> i()
              activate(n__o()) -> o()
              activate(n__u()) -> u()
              activate(X) -> X
            Matrix Interpretation Processor:
             dimension: 1
             max_matrix:
              1
              interpretation:
               [u] = 56,
               
               [o] = 60,
               
               [i] = 57,
               
               [e] = 56,
               
               [a] = 56,
               
               [n__u] = 56,
               
               [n__o] = 60,
               
               [n__i] = 56,
               
               [n__e] = 56,
               
               [n__a] = 56,
               
               [isPal](x0) = x0 + 8,
               
               [n__isPal](x0) = x0 + 8,
               
               [isNePal](x0) = x0 + 2,
               
               [n__isNeList](x0) = x0,
               
               [isQid](x0) = x0,
               
               [n__isList](x0) = x0 + 3,
               
               [n____](x0, x1) = x0 + x1 + 54,
               
               [n__nil] = 58,
               
               [isNeList](x0) = x0 + 1,
               
               [isList](x0) = x0 + 4,
               
               [activate](x0) = x0 + 1,
               
               [and](x0, x1) = x0 + x1 + 6,
               
               [tt] = 56,
               
               [nil] = 59,
               
               [__](x0, x1) = x0 + x1
              orientation:
               __(__(X,Y),Z) = X + Y + Z >= X + Y + Z = __(X,__(Y,Z))
               
               nil() = 59 >= 58 = n__nil()
               
               __(X1,X2) = X1 + X2 >= X1 + X2 + 54 = n____(X1,X2)
               
               isList(n____(V1,V2)) = V1 + V2 + 58 >= V1 + V2 + 15 = and(isList(activate(V1)),n__isList(activate(V2)))
               
               isNeList(n____(V1,V2)) = V1 + V2 + 55 >= V1 + V2 + 12 = and(isNeList(activate(V1)),n__isList(activate(V2)))
               
               isList(X) = X + 4 >= X + 3 = n__isList(X)
               
               e() = 56 >= 56 = n__e()
               
               isList(V) = V + 4 >= V + 2 = isNeList(activate(V))
               
               o() = 60 >= 60 = n__o()
               
               isNeList(V) = V + 1 >= V + 1 = isQid(activate(V))
               
               isNeList(n____(V1,V2)) = V1 + V2 + 55 >= V1 + V2 + 12 = and(isList(activate(V1)),n__isNeList(activate(V2)))
               
               isPal(V) = V + 8 >= V + 3 = isNePal(activate(V))
               
               isPal(X) = X + 8 >= X + 8 = n__isPal(X)
               
               a() = 56 >= 56 = n__a()
               
               and(tt(),X) = X + 62 >= X + 1 = activate(X)
               
               isNePal(V) = V + 2 >= V + 1 = isQid(activate(V))
               
               isNeList(X) = X + 1 >= X = n__isNeList(X)
               
               i() = 57 >= 56 = n__i()
               
               u() = 56 >= 56 = n__u()
               
               __(X,nil()) = X + 59 >= X = X
               
               __(nil(),X) = X + 59 >= X = X
               
               isList(n__nil()) = 62 >= 56 = tt()
               
               isNePal(n____(I,__(P,I))) = 2I + P + 56 >= I + P + 16 = and(isQid(activate(I)),n__isPal(activate(P)))
               
               isPal(n__nil()) = 66 >= 56 = tt()
               
               isQid(n__a()) = 56 >= 56 = tt()
               
               isQid(n__e()) = 56 >= 56 = tt()
               
               isQid(n__i()) = 56 >= 56 = tt()
               
               isQid(n__o()) = 60 >= 56 = tt()
               
               isQid(n__u()) = 56 >= 56 = tt()
               
               activate(n__nil()) = 59 >= 59 = nil()
               
               activate(n____(X1,X2)) = X1 + X2 + 55 >= X1 + X2 = __(X1,X2)
               
               activate(n__isList(X)) = X + 4 >= X + 4 = isList(X)
               
               activate(n__isNeList(X)) = X + 1 >= X + 1 = isNeList(X)
               
               activate(n__isPal(X)) = X + 9 >= X + 8 = isPal(X)
               
               activate(n__a()) = 57 >= 56 = a()
               
               activate(n__e()) = 57 >= 56 = e()
               
               activate(n__i()) = 57 >= 57 = i()
               
               activate(n__o()) = 61 >= 60 = o()
               
               activate(n__u()) = 57 >= 56 = u()
               
               activate(X) = X + 1 >= X = X
              problem:
               strict:
                __(__(X,Y),Z) -> __(X,__(Y,Z))
                __(X1,X2) -> n____(X1,X2)
               weak:
                nil() -> n__nil()
                isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
                isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
                isList(X) -> n__isList(X)
                e() -> n__e()
                isList(V) -> isNeList(activate(V))
                o() -> n__o()
                isNeList(V) -> isQid(activate(V))
                isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
                isPal(V) -> isNePal(activate(V))
                isPal(X) -> n__isPal(X)
                a() -> n__a()
                and(tt(),X) -> activate(X)
                isNePal(V) -> isQid(activate(V))
                isNeList(X) -> n__isNeList(X)
                i() -> n__i()
                u() -> n__u()
                __(X,nil()) -> X
                __(nil(),X) -> X
                isList(n__nil()) -> tt()
                isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
                isPal(n__nil()) -> tt()
                isQid(n__a()) -> tt()
                isQid(n__e()) -> tt()
                isQid(n__i()) -> tt()
                isQid(n__o()) -> tt()
                isQid(n__u()) -> tt()
                activate(n__nil()) -> nil()
                activate(n____(X1,X2)) -> __(X1,X2)
                activate(n__isList(X)) -> isList(X)
                activate(n__isNeList(X)) -> isNeList(X)
                activate(n__isPal(X)) -> isPal(X)
                activate(n__a()) -> a()
                activate(n__e()) -> e()
                activate(n__i()) -> i()
                activate(n__o()) -> o()
                activate(n__u()) -> u()
                activate(X) -> X
              Matrix Interpretation Processor:
               dimension: 1
               max_matrix:
                1
                interpretation:
                 [u] = 0,
                 
                 [o] = 0,
                 
                 [i] = 0,
                 
                 [e] = 0,
                 
                 [a] = 0,
                 
                 [n__u] = 0,
                 
                 [n__o] = 0,
                 
                 [n__i] = 0,
                 
                 [n__e] = 0,
                 
                 [n__a] = 0,
                 
                 [isPal](x0) = x0 + 62,
                 
                 [n__isPal](x0) = x0 + 61,
                 
                 [isNePal](x0) = x0 + 39,
                 
                 [n__isNeList](x0) = x0 + 2,
                 
                 [isQid](x0) = x0 + 1,
                 
                 [n__isList](x0) = x0 + 4,
                 
                 [n____](x0, x1) = x0 + x1 + 18,
                 
                 [n__nil] = 0,
                 
                 [isNeList](x0) = x0 + 2,
                 
                 [isList](x0) = x0 + 4,
                 
                 [activate](x0) = x0 + 1,
                 
                 [and](x0, x1) = x0 + x1 + 12,
                 
                 [tt] = 0,
                 
                 [nil] = 0,
                 
                 [__](x0, x1) = x0 + x1 + 19
                orientation:
                 __(__(X,Y),Z) = X + Y + Z + 38 >= X + Y + Z + 38 = __(X,__(Y,Z))
                 
                 __(X1,X2) = X1 + X2 + 19 >= X1 + X2 + 18 = n____(X1,X2)
                 
                 nil() = 0 >= 0 = n__nil()
                 
                 isList(n____(V1,V2)) = V1 + V2 + 22 >= V1 + V2 + 22 = and(isList(activate(V1)),n__isList(activate(V2)))
                 
                 isNeList(n____(V1,V2)) = V1 + V2 + 20 >= V1 + V2 + 20 = and(isNeList(activate(V1)),n__isList(activate(V2)))
                 
                 isList(X) = X + 4 >= X + 4 = n__isList(X)
                 
                 e() = 0 >= 0 = n__e()
                 
                 isList(V) = V + 4 >= V + 3 = isNeList(activate(V))
                 
                 o() = 0 >= 0 = n__o()
                 
                 isNeList(V) = V + 2 >= V + 2 = isQid(activate(V))
                 
                 isNeList(n____(V1,V2)) = V1 + V2 + 20 >= V1 + V2 + 20 = and(isList(activate(V1)),n__isNeList(activate(V2)))
                 
                 isPal(V) = V + 62 >= V + 40 = isNePal(activate(V))
                 
                 isPal(X) = X + 62 >= X + 61 = n__isPal(X)
                 
                 a() = 0 >= 0 = n__a()
                 
                 and(tt(),X) = X + 12 >= X + 1 = activate(X)
                 
                 isNePal(V) = V + 39 >= V + 2 = isQid(activate(V))
                 
                 isNeList(X) = X + 2 >= X + 2 = n__isNeList(X)
                 
                 i() = 0 >= 0 = n__i()
                 
                 u() = 0 >= 0 = n__u()
                 
                 __(X,nil()) = X + 19 >= X = X
                 
                 __(nil(),X) = X + 19 >= X = X
                 
                 isList(n__nil()) = 4 >= 0 = tt()
                 
                 isNePal(n____(I,__(P,I))) = 2I + P + 76 >= I + P + 76 = and(isQid(activate(I)),n__isPal(activate(P)))
                 
                 isPal(n__nil()) = 62 >= 0 = tt()
                 
                 isQid(n__a()) = 1 >= 0 = tt()
                 
                 isQid(n__e()) = 1 >= 0 = tt()
                 
                 isQid(n__i()) = 1 >= 0 = tt()
                 
                 isQid(n__o()) = 1 >= 0 = tt()
                 
                 isQid(n__u()) = 1 >= 0 = tt()
                 
                 activate(n__nil()) = 1 >= 0 = nil()
                 
                 activate(n____(X1,X2)) = X1 + X2 + 19 >= X1 + X2 + 19 = __(X1,X2)
                 
                 activate(n__isList(X)) = X + 5 >= X + 4 = isList(X)
                 
                 activate(n__isNeList(X)) = X + 3 >= X + 2 = isNeList(X)
                 
                 activate(n__isPal(X)) = X + 62 >= X + 62 = isPal(X)
                 
                 activate(n__a()) = 1 >= 0 = a()
                 
                 activate(n__e()) = 1 >= 0 = e()
                 
                 activate(n__i()) = 1 >= 0 = i()
                 
                 activate(n__o()) = 1 >= 0 = o()
                 
                 activate(n__u()) = 1 >= 0 = u()
                 
                 activate(X) = X + 1 >= X = X
                problem:
                 strict:
                  __(__(X,Y),Z) -> __(X,__(Y,Z))
                 weak:
                  __(X1,X2) -> n____(X1,X2)
                  nil() -> n__nil()
                  isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
                  isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
                  isList(X) -> n__isList(X)
                  e() -> n__e()
                  isList(V) -> isNeList(activate(V))
                  o() -> n__o()
                  isNeList(V) -> isQid(activate(V))
                  isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
                  isPal(V) -> isNePal(activate(V))
                  isPal(X) -> n__isPal(X)
                  a() -> n__a()
                  and(tt(),X) -> activate(X)
                  isNePal(V) -> isQid(activate(V))
                  isNeList(X) -> n__isNeList(X)
                  i() -> n__i()
                  u() -> n__u()
                  __(X,nil()) -> X
                  __(nil(),X) -> X
                  isList(n__nil()) -> tt()
                  isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
                  isPal(n__nil()) -> tt()
                  isQid(n__a()) -> tt()
                  isQid(n__e()) -> tt()
                  isQid(n__i()) -> tt()
                  isQid(n__o()) -> tt()
                  isQid(n__u()) -> tt()
                  activate(n__nil()) -> nil()
                  activate(n____(X1,X2)) -> __(X1,X2)
                  activate(n__isList(X)) -> isList(X)
                  activate(n__isNeList(X)) -> isNeList(X)
                  activate(n__isPal(X)) -> isPal(X)
                  activate(n__a()) -> a()
                  activate(n__e()) -> e()
                  activate(n__i()) -> i()
                  activate(n__o()) -> o()
                  activate(n__u()) -> u()
                  activate(X) -> X
                Matrix Interpretation Processor:
                 dimension: 2
                 max_matrix:
                  [1 2]
                  [0 1]
                  interpretation:
                         [1]
                   [u] = [0],
                   
                         [0]
                   [o] = [0],
                   
                         [2]
                   [i] = [1],
                   
                         [0]
                   [e] = [1],
                   
                         [0]
                   [a] = [1],
                   
                            [1]
                   [n__u] = [0],
                   
                            [0]
                   [n__o] = [0],
                   
                            [2]
                   [n__i] = [1],
                   
                            [0]
                   [n__e] = [1],
                   
                            [0]
                   [n__a] = [1],
                   
                                 [1 1]     [1]
                   [isPal](x0) = [0 1]x0 + [0],
                   
                                    [1 1]     [1]
                   [n__isPal](x0) = [0 1]x0 + [0],
                   
                                   [1 1]     [1]
                   [isNePal](x0) = [0 1]x0 + [0],
                   
                                         
                   [n__isNeList](x0) = x0,
                   
                                   
                   [isQid](x0) = x0,
                   
                                       
                   [n__isList](x0) = x0,
                   
                                     [1 2]          [2]
                   [n____](x0, x1) = [0 1]x0 + x1 + [3],
                   
                              [0]
                   [n__nil] = [0],
                   
                                      
                   [isNeList](x0) = x0,
                   
                                    
                   [isList](x0) = x0,
                   
                                      
                   [activate](x0) = x0,
                   
                                   [1 2]          [1]
                   [and](x0, x1) = [0 0]x0 + x1 + [2],
                   
                          [0]
                   [tt] = [0],
                   
                           [0]
                   [nil] = [0],
                   
                                  [1 2]          [2]
                   [__](x0, x1) = [0 1]x0 + x1 + [3]
                  orientation:
                                   [1 4]    [1 2]        [10]    [1 2]    [1 2]        [4]                
                   __(__(X,Y),Z) = [0 1]X + [0 1]Y + Z + [6 ] >= [0 1]X + [0 1]Y + Z + [6] = __(X,__(Y,Z))
                   
                               [1 2]          [2]    [1 2]          [2]               
                   __(X1,X2) = [0 1]X1 + X2 + [3] >= [0 1]X1 + X2 + [3] = n____(X1,X2)
                   
                           [0]    [0]           
                   nil() = [0] >= [0] = n__nil()
                   
                                          [1 2]          [2]    [1 2]          [1]                                                    
                   isList(n____(V1,V2)) = [0 1]V1 + V2 + [3] >= [0 0]V1 + V2 + [2] = and(isList(activate(V1)),n__isList(activate(V2)))
                   
                                            [1 2]          [2]    [1 2]          [1]                                                      
                   isNeList(n____(V1,V2)) = [0 1]V1 + V2 + [3] >= [0 0]V1 + V2 + [2] = and(isNeList(activate(V1)),n__isList(activate(V2)))
                   
                                                    
                   isList(X) = X >= X = n__isList(X)
                   
                         [0]    [0]         
                   e() = [1] >= [1] = n__e()
                   
                                                             
                   isList(V) = V >= V = isNeList(activate(V))
                   
                         [0]    [0]         
                   o() = [0] >= [0] = n__o()
                   
                                                            
                   isNeList(V) = V >= V = isQid(activate(V))
                   
                                            [1 2]          [2]    [1 2]          [1]                                                      
                   isNeList(n____(V1,V2)) = [0 1]V1 + V2 + [3] >= [0 0]V1 + V2 + [2] = and(isList(activate(V1)),n__isNeList(activate(V2)))
                   
                              [1 1]    [1]    [1 1]    [1]                       
                   isPal(V) = [0 1]V + [0] >= [0 1]V + [0] = isNePal(activate(V))
                   
                              [1 1]    [1]    [1 1]    [1]              
                   isPal(X) = [0 1]X + [0] >= [0 1]X + [0] = n__isPal(X)
                   
                         [0]    [0]         
                   a() = [1] >= [1] = n__a()
                   
                                     [1]                   
                   and(tt(),X) = X + [2] >= X = activate(X)
                   
                                [1 1]    [1]                          
                   isNePal(V) = [0 1]V + [0] >= V = isQid(activate(V))
                   
                                                        
                   isNeList(X) = X >= X = n__isNeList(X)
                   
                         [2]    [2]         
                   i() = [1] >= [1] = n__i()
                   
                         [1]    [1]         
                   u() = [0] >= [0] = n__u()
                   
                                 [1 2]    [2]         
                   __(X,nil()) = [0 1]X + [3] >= X = X
                   
                                     [2]         
                   __(nil(),X) = X + [3] >= X = X
                   
                                      [0]    [0]       
                   isList(n__nil()) = [0] >= [0] = tt()
                   
                                               [2 4]    [1 3]    [11]    [1 2]    [1 1]    [2]                                                
                   isNePal(n____(I,__(P,I))) = [0 2]I + [0 1]P + [6 ] >= [0 0]I + [0 1]P + [2] = and(isQid(activate(I)),n__isPal(activate(P)))
                   
                                     [1]    [0]       
                   isPal(n__nil()) = [0] >= [0] = tt()
                   
                                   [0]    [0]       
                   isQid(n__a()) = [1] >= [0] = tt()
                   
                                   [0]    [0]       
                   isQid(n__e()) = [1] >= [0] = tt()
                   
                                   [2]    [0]       
                   isQid(n__i()) = [1] >= [0] = tt()
                   
                                   [0]    [0]       
                   isQid(n__o()) = [0] >= [0] = tt()
                   
                                   [1]    [0]       
                   isQid(n__u()) = [0] >= [0] = tt()
                   
                                        [0]    [0]        
                   activate(n__nil()) = [0] >= [0] = nil()
                   
                                            [1 2]          [2]    [1 2]          [2]            
                   activate(n____(X1,X2)) = [0 1]X1 + X2 + [3] >= [0 1]X1 + X2 + [3] = __(X1,X2)
                   
                                                              
                   activate(n__isList(X)) = X >= X = isList(X)
                   
                                                                  
                   activate(n__isNeList(X)) = X >= X = isNeList(X)
                   
                                           [1 1]    [1]    [1 1]    [1]           
                   activate(n__isPal(X)) = [0 1]X + [0] >= [0 1]X + [0] = isPal(X)
                   
                                      [0]    [0]      
                   activate(n__a()) = [1] >= [1] = a()
                   
                                      [0]    [0]      
                   activate(n__e()) = [1] >= [1] = e()
                   
                                      [2]    [2]      
                   activate(n__i()) = [1] >= [1] = i()
                   
                                      [0]    [0]      
                   activate(n__o()) = [0] >= [0] = o()
                   
                                      [1]    [1]      
                   activate(n__u()) = [0] >= [0] = u()
                   
                                           
                   activate(X) = X >= X = X
                  problem:
                   strict:
                    
                   weak:
                    __(__(X,Y),Z) -> __(X,__(Y,Z))
                    __(X1,X2) -> n____(X1,X2)
                    nil() -> n__nil()
                    isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
                    isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
                    isList(X) -> n__isList(X)
                    e() -> n__e()
                    isList(V) -> isNeList(activate(V))
                    o() -> n__o()
                    isNeList(V) -> isQid(activate(V))
                    isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
                    isPal(V) -> isNePal(activate(V))
                    isPal(X) -> n__isPal(X)
                    a() -> n__a()
                    and(tt(),X) -> activate(X)
                    isNePal(V) -> isQid(activate(V))
                    isNeList(X) -> n__isNeList(X)
                    i() -> n__i()
                    u() -> n__u()
                    __(X,nil()) -> X
                    __(nil(),X) -> X
                    isList(n__nil()) -> tt()
                    isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
                    isPal(n__nil()) -> tt()
                    isQid(n__a()) -> tt()
                    isQid(n__e()) -> tt()
                    isQid(n__i()) -> tt()
                    isQid(n__o()) -> tt()
                    isQid(n__u()) -> tt()
                    activate(n__nil()) -> nil()
                    activate(n____(X1,X2)) -> __(X1,X2)
                    activate(n__isList(X)) -> isList(X)
                    activate(n__isNeList(X)) -> isNeList(X)
                    activate(n__isPal(X)) -> isPal(X)
                    activate(n__a()) -> a()
                    activate(n__e()) -> e()
                    activate(n__i()) -> i()
                    activate(n__o()) -> o()
                    activate(n__u()) -> u()
                    activate(X) -> X
                  Qed